\begin{tabbing}
$\forall$\=$T$:($i$:Id$\rightarrow$\{$k$:Knd$\mid$ $\uparrow$hasloc($k$;$i$)\} $\rightarrow$Type), $P$:($i$:Id$\rightarrow$$k$:\{$k$:Knd$\mid$ $\uparrow$hasloc($k$;$i$)\} $\rightarrow$$T$($i$,$k$)),\+
\\[0ex]${\it ik}$:LocKnd.
\-\\[0ex]let $i$,$k$:LocKnd = ${\it ik}$ in $P$($i$,$k$) $\in$ $T$(${\it ik}$.1,${\it ik}$.2)
\end{tabbing}